(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

a(b(c(x1))) → a(a(b(x1)))
a(b(c(x1))) → b(c(b(c(x1))))
a(b(c(x1))) → c(b(c(a(x1))))

Rewrite Strategy: INNERMOST

(1) CpxTrsMatchBoundsProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 3.
The certificate found is represented by the following graph.
Start state: 1253
Accept states: [1254]
Transitions:
1253→1254[a_1|0]
1253→1253[b_1|0, c_1|0]
1253→1255[b_1|1]
1253→1257[c_1|1]
1253→1260[a_1|1]
1253→1272[b_1|2]
1253→1274[c_1|2]
1253→1277[a_1|2]
1255→1256[a_1|1]
1256→1254[a_1|1]
1256→1260[a_1|1]
1256→1256[a_1|1]
1256→1277[a_1|1]
1256→1273[a_1|1]
1257→1258[b_1|1]
1258→1259[c_1|1]
1258→1264[b_1|2]
1258→1266[c_1|2]
1258→1269[a_1|2]
1258→1280[b_1|3]
1258→1282[c_1|3]
1258→1285[a_1|3]
1259→1254[b_1|1]
1259→1260[b_1|1]
1259→1256[b_1|1]
1259→1277[b_1|1]
1259→1273[b_1|1]
1260→1261[c_1|1]
1261→1262[b_1|1]
1262→1254[c_1|1]
1262→1260[c_1|1]
1262→1256[c_1|1]
1262→1277[c_1|1]
1262→1273[c_1|1]
1264→1265[a_1|2]
1265→1254[a_1|2]
1265→1260[a_1|2]
1265→1256[a_1|2]
1265→1277[a_1|2]
1265→1273[a_1|2]
1265→1269[a_1|2]
1265→1285[a_1|2]
1266→1267[b_1|2]
1267→1268[c_1|2]
1267→1264[b_1|2]
1267→1266[c_1|2]
1267→1269[a_1|2]
1267→1280[b_1|3]
1267→1282[c_1|3]
1267→1285[a_1|3]
1268→1254[b_1|2]
1268→1260[b_1|2]
1268→1256[b_1|2]
1268→1277[b_1|2]
1268→1273[b_1|2]
1268→1269[b_1|2]
1268→1285[b_1|2]
1269→1270[c_1|2]
1270→1271[b_1|2]
1271→1254[c_1|2]
1271→1260[c_1|2]
1271→1256[c_1|2]
1271→1277[c_1|2]
1271→1273[c_1|2]
1271→1269[c_1|2]
1271→1285[c_1|2]
1272→1273[a_1|2]
1273→1269[a_1|2]
1273→1285[a_1|2]
1274→1275[b_1|2]
1275→1276[c_1|2]
1276→1269[b_1|2]
1276→1285[b_1|2]
1277→1278[c_1|2]
1278→1279[b_1|2]
1279→1269[c_1|2]
1279→1285[c_1|2]
1280→1281[a_1|3]
1281→1269[a_1|3]
1281→1285[a_1|3]
1282→1283[b_1|3]
1283→1284[c_1|3]
1284→1269[b_1|3]
1284→1285[b_1|3]
1285→1286[c_1|3]
1286→1287[b_1|3]
1287→1269[c_1|3]
1287→1285[c_1|3]

(2) BOUNDS(O(1), O(n^1))